package tableaux.rules;

import java.util.ArrayList;
import java.util.HashMap;
import java.util.HashSet;
import java.util.List;
import java.util.Map;
//import java.util.Map;
import java.util.Set;

import option.KBVocabulary;

import algebra.rewriting.kfree.LangPd;

import preprocessor.Simplification;
import preprocessor.absorption.Absorption;
import preprocessor.absorption.extended.OptimizedRestrictions;
import tableaux.*;
import tableaux.backjumping.DependencyImp;
import tableaux.backjumping.DependencyImpMax;
import utils.exception.CoreReasoningException;

import kb.TBox;
import entities.Individual;
import entities.concept.*;
import entities.role.Role;

public class RuleLazyUnfolding {
	// if no dep set for feature guards, they are considered to be always on the
	// TOP level (branch=0)
	// private static boolean fguardsNoDepSet
	// =
	// InitParam.getProperty("dependency.feature.guard.excluded").trim().equalsIgnoreCase("true");

	private Completion dc;
	private Branching br;
	private TBox tb;
	private boolean TuAxiom = false, TnuAxiom = false, TbAxiom = false,
			featureRule = false, TgAxiom = false, TfAxiom = false, Tbgeneral = false;
	// domainRange = false;
//	private static boolean featureAxiom = false;
	private HashSet<Concept> unexpanded;
	private Set<Concept> gcis;

//	public static void clearGCIsTransformed(){
//		gcis = null;
//	}
	
	public RuleLazyUnfolding(Completion dc) {
		super();
		this.dc = dc;
		this.br = this.dc.getCurrentBranching();
		this.tb = dc.getInitTBox();
//		if (gcis == null) {
//			gcis = this.applyGCIs();
//		}
		gcis = this.tb.getTgAsSet();
		// featureAxiom = this.tb.getGciFeatures().size()>0 ||
		// this.tb.getAxiomFeatures().size()>0;
	}
	
	private static Set<Role> TfFeatures = new HashSet<Role>();
	private static Set<String> TfValues = new HashSet<String>();
	public static void clearTfFeatureValues(){
		TfFeatures.clear();
		TfValues.clear();
	}
	public static void addTfFeature(Role f){
		TfFeatures.add(f);
	}
	public static void addTfValue(String v){
		TfValues.add(v);
	}
	public static void addTfValues(Set<String> vs){
		TfValues.addAll(vs);
	}
	
	private void analyzeTfRule(Individual n, Set<Concept> newLabels){
		String gv = KBVocabulary.AnyStringInKB;
		this.populateUnexp(n);
		Set<DomainConcept<?,?>> todo = new HashSet<DomainConcept<?,?>>();
		//in fact, f may be paired with more than one value, I suspect that rarely happens in reality.
		Map<Role, String> fvs = new HashMap<Role, String>();
		for (Concept uc : this.unexpanded) {
			if (uc instanceof DomainConcept) {
				DomainConcept<?, ?> dc = (DomainConcept<?, ?>) uc;
				Role f = (Role) dc.getRealFeature();
				if(f!= null && ! TfFeatures.contains(f)){
					continue;
				}
				String v = (String) dc.getRealValue();
				if(!v.equals(gv)){
					if(TfValues.contains(v)){
						fvs.put(f, v);
					}
					continue;
				}
				todo.add(dc);
			}
		}
		Concept addc = null;
		for(DomainConcept<?,?> dc:todo){
			//replace ? by a proper value
			Role f = (Role) dc.getRealFeature();
			if(fvs.containsKey(f)){
				String v = fvs.get(f);
				addc = dc.replaceValue(gv, v);
//				System.err.println("replaced "+dc+" by: "+addc);
				sucAddCp(n, addc, dc, newLabels);
			}
		}
	}

	public boolean isApplicable(Individual n) {
		// if(! n.hasAppliedGCI() && tb.getTg().size()>0){
		// this.TgAxiom = true;
		// }
//		if (tb.getTg().size() > 0) {
		if (gcis != null & gcis.size() > 0) {
			this.TgAxiom = !(n.getLabels().containsAll(gcis));
		}

		// special TBox for computing Lq
		if (LangPd.useStarToReplaceConstants && n.getTfKeyChange()) {
			TfAxiom = true;
			n.unsetTfKeyChange();
		}

		if (Absorption.CA && n.getCnKeyAddedChange()) {
			this.TuAxiom = true;
			this.populateUnexp(n);
			n.unsetCnKeyAddedChange();
		}
		if (Absorption.NCA && n.getCnNegKeyAddedChange()) {
			this.TnuAxiom = true;
			this.populateUnexp(n);
			n.unsetCnNegKeyAddedChange();
		}
		// binary axioms get fired only if an atomic concept is added
		if (OptimizedRestrictions.OptimizeEx && Absorption.BA && n.getGeneralBinaryKeyAddedChange()
				&& this.generalBinaryToBeFired(n)) {
			this.Tbgeneral = true;
			getPrimConceptsInLabel(n);
			n.unsetGeneralBinaryKeyAddedChanges();
		}
		if (Absorption.BA && n.getBinaryKeyAddedChange()
				&& this.limitedBinaryToBeFired(n)) {
			this.TbAxiom = true;
			getPrimConceptsInLabel(n);
			n.unsetBinaryKeyAddedChanges(); // waiting for next atomic concepts
		}
		// version 1: features are generated by rules
		if (Completion.featureGuardsInRule && n.getDomainKeyAddedChange()
				&& this.featureGuardRuleApplicable(n)) {
			this.featureRule = true;
			n.unsetDomainKeyAddedChange();
		}
		// if(Absorption.RA){
		// for(Role r:n.getChildrenMap().keySet()){
		// if(RoleAbsorption.getAbsorbedDomainRangeAxioms().containsKey(r)){
		// Concept toadd = RoleAbsorption.getAbsorbedDomainRangeAxioms().get(r);
		// for(Individual i:n.getChildren(r)){
		// if(!i.getLabels().contains(toadd)){
		// this.domainRange = true;
		// }
		// }
		// }
		// }
		//
		// }

		// if(Absorption.RA &&
		// !Collections.disjoint(n.getChildrenMap().keySet(),
		// RoleAbsorption.getAbsorbedDomainRangeAxioms().keySet())){
		// this.domainRange = true;
		// }
		return this.TnuAxiom || this.TuAxiom || this.TbAxiom
				|| this.featureRule || TgAxiom || TfAxiom;
	}

	private Set<Concept> noms, guards, pcs;
	private void getPrimConceptsInLabel(Individual n){
		if(noms!=null || guards!=null || pcs!=null){
			//already populated
			return;
		}
		noms = new HashSet<Concept>();
		guards = new HashSet<Concept>();
		pcs = new HashSet<Concept>();
		for (Concept c : n.getLabels()) {
			if(!  (c instanceof AtomicConcept)){
				continue;
			}
			if (c instanceof Nominal) {
				noms.add((Nominal) c);
			} else if(c.isGuard()) {
				guards.add(c);
			} else{
				pcs.add(c);
			}
		}
	}
	
	private Set<Concept> toBinaryLabel = null;
	private List<PConcept> binaryTriggers = null;
	//for this not-so-general binary absorption: DEF_role and A -> C
	private boolean generalBinaryToBeFired(Individual n) {
		boolean ret = false;
		if (guards == null || guards.size() < 1) {
			return false;
		}
		if (pcs == null || pcs.size() < 1) {
			return false;
		}
		for (Concept e : guards) {
			if(!e.isRoleGuard()){
				continue;
			}
			PConcept defr = (PConcept) e;
			for (Concept p : pcs) {
				// check if the pair is in binary axioms
				boolean fired = n.hasFiredGeneralBinaryEntry(defr, (PConcept) p);
				if (fired) {
					continue;
				}
				Concept add = tb.getLessSpecialBinaryClass().getEntry(defr, (PConcept)p);
				if (add != null) {
					// this entry needs to be fired
					if (toBinaryLabel == null) {
						toBinaryLabel = new HashSet<Concept>();
					}
					toBinaryLabel.add(add);
					if (binaryTriggers == null) {
						binaryTriggers = new ArrayList<PConcept>();
					}
					binaryTriggers.add(defr);
					binaryTriggers.add((PConcept)p);
					if (Completion.DEP_MAX) {
						DependencyImpMax.addDep(n, add,
								DependencyImpMax.getDepOfConcept(n, defr));
						DependencyImpMax.addDep(n, add,
								DependencyImpMax.getDepOfConcept(n, p));
					} else {
						DependencyImp.setDep(n, add,
								DependencyImp.getDepSetOfConcept(n, defr));
						DependencyImp.setDep(n, add,
								DependencyImp.getDepSetOfConcept(n, p));
					}
					ret = true;
				}
			}
		}
		return ret;
	}

	private void populateUnexp(Individual n) {
		if (this.unexpanded != null) {
			return;
		}
		HashSet<Concept> unexp = new HashSet<Concept>();
		unexp.addAll(n.getLabels());
		unexp.removeAll(n.getUnfolededLabels());
		unexpanded = unexp;
	}

	private void sucAddCp(Individual ind, Concept addc, Concept c,
			Set<Concept> newLabels) {
		if (ind.getLabels().contains(addc)) {
			return;
		}
		boolean sucadd = ind.addUnfoldedLabels(c);
		if (BranchChanges.getRecordingStatus() && sucadd) {
			br.getBranchChanges().addToUnfoldedLabels(ind, c);
		}
		newLabels.add(addc);
		// add dependency
		if (Completion.DEP_MAX) {
			DependencyImpMax.addDep(ind, addc,
					DependencyImpMax.getDepOfConcept(ind, c));
		} else {
			DependencyImp.setDep(ind, addc,
					DependencyImp.getDepSetOfConcept(ind, c));
		}
	}

	public boolean applyRule(Individual ind) {
		boolean suc = false;
		Set<Concept> newLabels = new HashSet<Concept>();
		if (this.TgAxiom) {
			newLabels.addAll(gcis);
		}
		// for special TBox used in Lq
		if (this.TfAxiom) {
//			for (Concept c : this.unexpanded) {
//				if (c instanceof DomainConcept<?, ?>
//						&& tb.getTf().containsKey(c)) {
//					for (Concept addc : tb.getTf().get(c)) {
//						sucAddCp(ind, addc, c, newLabels);
//					}
//				}
//			}
			analyzeTfRule(ind, newLabels);
		}

		//
		if (this.TuAxiom) {
			// apply unary axioms
			for (Concept c : this.unexpanded) {
				if (c instanceof AtomicConcept
						&& this.tb.getTu().containsKey(c)) {
					Concept addc = tb.getTu().get(c);
					sucAddCp(ind, addc, c, newLabels);
				}
			}
		}
		if (this.TnuAxiom) {
			for (Concept c : this.unexpanded) {
				if (c instanceof NotConcept && this.tb.getTnu().containsKey(c)) {
					Concept addc = tb.getTnu().get(c);
					sucAddCp(ind, addc, c, newLabels);
				}
			}
		}
		if (this.TbAxiom) {
			// dependencies added only for limited binary axioms
			if (toLabel != null && toLabel.size() > 0) {
				newLabels.addAll(toLabel);
			}
			if (triggers != null && triggers.size() > 0) {
				for (int i = 0; i < triggers.size(); i += 2) {
					AtomicConcept c1 = triggers.get(i), c2 = triggers
							.get(i + 1);
					try {
						ind.addBinaryExpanded(c1, c2);
						if (BranchChanges.getRecordingStatus()) {
							br.getBranchChanges().addToBinaryFired(ind, c1, c2);
						}
					} catch (CoreReasoningException e) {
						e.printStackTrace();
					}
				}
			}
		}
		if (this.Tbgeneral) {
			if (toBinaryLabel != null && toBinaryLabel.size() > 0) {
				newLabels.addAll(toBinaryLabel);
			}
			if (binaryTriggers != null && binaryTriggers.size() > 0) {
				for (int i = 0; i < binaryTriggers.size(); i += 2) {
					PConcept c1 = binaryTriggers.get(i), c2 = binaryTriggers
							.get(i + 1);
					try {
						ind.addGeneralBinaryExpanded(c1, c2);
						if (BranchChanges.getRecordingStatus()) {
							br.getBranchChanges().addToGeneralBinaryFiredEntry(ind, c1, c2);
						}
					} catch (CoreReasoningException e) {
						e.printStackTrace();
					}
				}
			}
		}
		// //apply binary axioms, note that the expanded concepts are not added
		// //to expandedLabels (as they may be reused) instead they are stored
		// in the node's binaryExpanded
		// for(HashSet<AtomicConcept> s:tb.getTb().keySet()){
		// if(ind.getLabels().containsAll(s)){
		// Concept addc = tb.getTb().get(s);
		// if(!ind.getLabels().contains(addc)){
		// newLabels.add(addc);
		// HashSet<Concept> ns = new HashSet<Concept>();
		// ns.addAll(s);
		// ind.addBinaryExpanded(ns);
		// if(BranchChanges.getRecordingStatus()){
		// for(Concept c:ns){
		// br.getBranchChanges().addToUnfoldedLabels(ind, c);
		// }
		//
		// }
		// }
		// }
		// }
		if (this.featureRule) {
			if (domainGuardsToLabel.size() > 0) {
				newLabels.addAll(domainGuardsToLabel);
			}
			if (this.unfoldedDomainConcepts.size() > 0) {
				if (BranchChanges.getRecordingStatus()) {
					for (Concept c : unfoldedDomainConcepts) {
						br.getBranchChanges().addToUnfoldedLabels(ind, c);
					}
				}
			}
		}

		for (Concept lb : newLabels) {
			if (ind.addLabels(lb)) {
				if (BranchChanges.getRecordingStatus()) {
					br.getBranchChanges().addToLabel(ind, lb);
				}
			}
		}
		// ind.addLabels(newLabels);
		suc = !newLabels.isEmpty();
		return suc;
	}

	private Set<Concept> toLabel = null;
	private List<AtomicConcept> triggers = null;

	private boolean limitedBinaryToBeFired(Individual n) {
		boolean ret = false;
		// if(!n.getBinaryKeyAddedChange()){
		// //no new atomic concepts were added, quit
		// return false;
		// }
		Set<Concept> labels = n.getLabels();
		Set<AtomicConcept> def = new HashSet<AtomicConcept>();
		Set<Nominal> nom = new HashSet<Nominal>();
		for (Concept c : labels) {
			if (c instanceof Nominal) {
				nom.add((Nominal) c);
			} else if (c instanceof AtomicConcept) {
				def.add((AtomicConcept) c);
			}
		}
		// tricks: one nominal must be paired with one def
		if (nom.size() < 1 || def.size() < 1) {
			return false;
		}
		for (AtomicConcept dc : def) {
			for (Nominal o : nom) {
				// check if the pair is in binary axioms
				boolean fired = n.hasFiredBinaryEntry(dc, o);
				if (fired) {
					continue;
				}
				Concept add = tb.getSpecialBinaryClass().getEntry(dc, o);
				if (add != null) {
					// this entry needs to be fired
					if (toLabel == null) {
						toLabel = new HashSet<Concept>();
					}
					toLabel.add(add);
					if (triggers == null) {
						triggers = new ArrayList<AtomicConcept>();
					}
					triggers.add(dc);
					triggers.add(o);
					// dependency for binary axioms
					if (Completion.DEP_MAX) {
						DependencyImpMax.addDep(n, add,
								DependencyImpMax.getDepOfConcept(n, dc));
						DependencyImpMax.addDep(n, add,
								DependencyImpMax.getDepOfConcept(n, o));
					} else {
						DependencyImp.setDep(n, add,
								DependencyImp.getDepSetOfConcept(n, dc));
						DependencyImp.setDep(n, add,
								DependencyImp.getDepSetOfConcept(n, o));
					}
					ret = true;
				}
			}
		}
		return ret;
	}

	// private Set<PConcept> getFeatureInAxioms() {
	// Set<PConcept> ret = new HashSet<PConcept>();
	// // no dependencies for GCI features
	// if(this.tb.getGciFeatures().size()>0){
	// for(Concept c:this.tb.getGciFeatures().keySet()){
	// Set<PConcept> deffs = this.tb.getGciFeatures().get(c);
	// ret.addAll(deffs);
	// }
	// }
	// //feature dependencies from LHS concepts
	// if(this.tb.getAxiomFeatures().size()>0){
	//
	// }
	// return;
	// }

	private Set<Concept> domainGuardsToLabel = null;
	private Set<Concept> unfoldedDomainConcepts = null;

	public boolean featureGuardRuleApplicable(Individual n) {
		// applicable only if a new domain concept is added to the node label
		// if(!n.getDomainKeyAddedChange()){
		// return false;
		// }
		// test if any new guards can be added to the node label
		this.populateUnexp(n);
		for (Concept uc : this.unexpanded) {
			if (uc instanceof DomainConcept) {
				DomainConcept<?, ?> dc = (DomainConcept<?, ?>) uc;
				for (AtomicConcept ac : this.getDomainConceptGuards(dc)) {
					if (!n.getLabels().contains(ac)) {
						if (domainGuardsToLabel == null) {
							domainGuardsToLabel = new HashSet<Concept>();
						}
						if (unfoldedDomainConcepts == null) {
							unfoldedDomainConcepts = new HashSet<Concept>();
						}
						domainGuardsToLabel.add(ac);
						if (Completion.DEP_MAX) {
							DependencyImpMax.addDep(n, ac,
									DependencyImpMax.getDepOfConcept(n, dc));
						} else {
							DependencyImp.setDep(n, ac,
									DependencyImp.getDepSetOfConcept(n, dc));
						}
						// DependencyImp.setDep(n, ac,
						// DependencyImp.getDepSetOfConcept(n, dc));
						// add dependencies for ac
						// if(tb.getAxiomFeatures().contains(dc)){
						// DependencyImp.setDep(n, ac,
						// DependencyImp.getDepSetOfConcept(n, dc));
						// //
						// System.out.println("DEP added: "+n+"; "+ac+" from "+dc+" depends on "
						// // +DependencyImp.getDepSetOfConcept(n, dc));
						// }
						//
						unfoldedDomainConcepts.add(dc);
					}
				}
			}
		}

		return domainGuardsToLabel != null && domainGuardsToLabel.size() > 0;
	}

	private static Map<DomainConcept<?, ?>, Set<AtomicConcept>> featureGuards = new HashMap<DomainConcept<?, ?>, Set<AtomicConcept>>();

	private Set<AtomicConcept> getDomainConceptGuards(DomainConcept<?, ?> dc) {
		if (featureGuards.containsKey(dc)) {
			return featureGuards.get(dc);
		}
		Set<AtomicConcept> rs = new HashSet<AtomicConcept>();
		for (Role f : dc.extractFeatures()) {
			rs.add(PConcept.newGuardPConcept(f));
		}
		featureGuards.put(dc, rs);
		return rs;
	}

//	private Set<Concept> applyGCIs() {
//		Set<Concept> newLabels = new HashSet<Concept>();
//		for (Concept k : this.tb.getTg().keySet()) {
//			if (k.isTop()) {
//				newLabels.add(this.tb.getTg().get(k));
//			} else {
//				newLabels.add(new OrConcept(Simplification.NNF(
//						new NotConcept(k), false), this.tb.getTg().get(k)));
//			}
//		}
//		return newLabels;
//	}

}
